es:ES, e:E.
isrcv(e)
 (index(e) = 0
 (
 ((e':E. isrcv(e')  sender(e') = sender(e)  E  lnk(e) = lnk(e')  IdLnk  e  e' )) 

latex

Definitions

ES, t  T, x:A. B(x), E, isrcv(e), b, e  e' , P  Q, lnk(e), IdLnk, s = t, Prop, x:AB(x), sender(e), Type, #$n, index(e), <a,b>, , sends(l;e), (Msg on l), ||as||, {i..j}, {x:A| B(x) }, P  Q, P & Q, P  Q, P  Q, (e <loc e'), loc(e), Id, Void, False, A, x:AB(x), A/x,y. B(x;y), 1of(t), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, True, T, destination(l), source(l), left+right, ij, {T}, Dec(P), a<b, AB, i  j < k, A & B, x:A. B(x)

Lemmas

es-le-trans2, le wf, decidable int equal, es-locl wf, es-locl-antireflexive, non neg length, es-axioms, lsrc wf, ldst wf, es-loc wf, squash wf, true wf, es-loc-pred, es-index wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-sender wf, IdLnk wf, es-lnk wf, es-le wf, assert wf, es-isrcv wf, es-E wf, event system wf